(agda2-status-action "")
(agda2-info-action "*Type-checking*" "" nil)
(agda2-highlight-clear)
(agda2-status-action "")
(agda2-info-action "*All Goals*" "?0 : _9 ?1 : ?0 (n = n) Sort _9 [ at Issue5210.agda:9,20-27 ] " nil)
((last . 1) . (agda2-goals-action '(0 1)))
(agda2-info-action "*Error*" "Issue5210.agda:10,12-20 Cannot split on datatype in Prop unless target is in Prop when checking that the expression ? has type ?0 (n = n)" nil)
((last . 3) . (agda2-maybe-goto '("Issue5210.agda" . 151)))
(agda2-highlight-load-and-delete-action)
(agda2-status-action "")
